Nuprl Lemma : atom-free-decl-single
0,22
postcript
pdf
T
,
A
:Type,
x
:
T
,
eq
:EqDecider(
T
). AtomFree(Type;
A
)
AtomFree(
x
:
A
)
latex
Definitions
t
T
,
false
,
x
:
A
.
B
(
x
)
,
eqof(
d
)
,
f
(
a
)
,
p
q
,
b
,
P
Q
,
f
(
x
)
,
x
dom(
f
)
,
x
dom(
f
).
v
=
f
(
x
)
P
(
x
;
v
)
,
x
:
v
,
Type
,
EqDecider(
T
)
,
AtomFree(
T
;
x
)
,
AtomFree(
d
)
Lemmas
atom-free
wf
,
deq
wf
,
assert
wf
,
bor
wf
,
eqof
wf
,
bfalse
wf
origin
T, A:Type, x:T, eq:EqDecider(T). AtomFree(Type;A) 
AtomFree(x : A) T, A:Type, x:T, eq:EqDecider(T). AtomFree(Type;A) AtomFree(x : A) 
T
x:A. B(x)
q
b Q dom(f)xdom(f). v=f(x) P(x;v)